| 1. Identificação | ||||
| Tipo de Referência | Artigo em Revista Científica (Journal Article) | |||
| Site | mtc-m16d.sid.inpe.br | |||
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S | |||
| Identificador | 8JMKD3MGP7W/3CEUM48 | |||
| Repositório | sid.inpe.br/mtc-m19/2012/08.15.16.22 (acesso restrito) | |||
| Última Atualização | 2012:08.15.16.25.18 (UTC) administrator | |||
| Repositório de Metadados | sid.inpe.br/mtc-m19/2012/08.15.16.22.47 | |||
| Última Atualização dos Metadados | 2021:02.11.21.04.56 (UTC) administrator | |||
| Chave Secundária | INPE--PRE/ | |||
| DOI | 10.1007/s10664-012-9215-y | |||
| ISSN | 1382-3256 | |||
| Chave de Citação | PontesVéraAmbrVill:2014:CoMoCh | |||
| Título | Contributions of model checking and CoFI methodology to the development of space embedded software  | |||
| Projeto | CNPq (306259/2011-7). | |||
| Ano | 2014 | |||
| Mês | Feb. | |||
| Data de Acesso | 27 abr. 2024 | |||
| Tipo de Trabalho | journal article | |||
| Tipo Secundário | PRE PI | |||
| Número de Arquivos | 1 | |||
| Tamanho | 593 KiB | |||
| 2. Contextualização | ||||
| Autor | 1 Pontes, Rodrigo Pastl 2 Véras, Paulo Claudino 3 Ambrosio, Ana Maria 4 Villani, Emília | |||
| Identificador de Curriculo | 1 2 3 8JMKD3MGP5W/3C9JGH7 | |||
| Grupo | 1 2 3 DSS-ETE-INPE-MCTI-GOV-BR | |||
| Afiliação | 1 Instituto Tecnológico de Aeronáutica (ITA) 2 Instituto Tecnológico de Aeronáutica (ITA) 3 Instituto Nacional de Pesquisas Espaciais (INPE) 4 Instituto Tecnológico de Aeronáutica (ITA) | |||
| Endereço de e-Mail do Autor | 1 rpastl@gmail.com 2 pauloveras@gmail.com 3 ana.ambrosio@inpe.br 4 evillani@ita.br | |||
| Endereço de e-Mail | marcelo.pazos@inpe.br | |||
| Revista | Empirical Software Engineering | |||
| Volume | 19 | |||
| Número | 1 | |||
| Páginas | 39-68 | |||
| Nota Secundária | A1_ENGENHARIAS_III A2_CIÊNCIA_DA_COMPUTAÇÃO A2_ENGENHARIAS_IV | |||
| Histórico (UTC) | 2012-08-15 16:33:22 :: marciana -> administrator :: 2012 2012-11-22 00:33:51 :: administrator -> marciana :: 2012 2012-12-14 12:21:36 :: marciana -> administrator :: 2012 2014-06-02 16:33:06 :: administrator :: 2012 -> 2014 2021-02-11 21:04:56 :: administrator -> marcelo.pazos@inpe.br :: 2014 | |||
| 3. Conteúdo e estrutura | ||||
| É a matriz ou uma cópia? | é a matriz | |||
| Estágio do Conteúdo | concluido | |||
| Transferível | 1 | |||
| Tipo do Conteúdo | External Contribution | |||
| Tipo de Versão | publisher | |||
| Palavras-Chave | verification model checking model based testing embedded software Packet Utilization Standard (PUS) space application | |||
| Resumo | The role of embedded software in the last space accidents highlights the importance of verification and validation techniques for the development of space embedded software. In this context, this work analyses the contribution of two verification techniques applied to the onboard data handling software of space products. The first technique is model checking. The system is modeled by a set of timed automata and the verification of safety and liveness properties is performed using UPPAAL model checker. The verified model is then used to generate the embedded software. The second technique analyzed in this work is model based approach for the generation of test cases. The Conformance and Fault Injection (CoFI) testing methodology is used to guide the development of a set of Finite State Machine (FSM) models from the software specification. The test suite is automatically generated from the FSM models. The contributions of the two methodologies are analyzed based on the results provided by an experiment. Two software products are used as case study, each one implementing two services of the Packet Utilization Standard (PUS). These services represent the functionalities offered by a satellite onboard data handling computer. One of the products is developed with the aid of model checking, while the other is developed according to the practices currently used at the Instituto Nacional de Pesquisas Espaciais (INPE). Both software products are tested by the CoFI methodology. The experiment highlights the advantages and vulnerable points of model checking. It also demonstrates that the main contribution of CoFI testing methodology is to highlight problems related to situations that have not been considered in the software specification, such as the occurrence of inopportune events. This analysis helps to understand how different techniques can be integrated in the design of critical embedded software. | |||
| Área | ETES | |||
| Arranjo | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > DIDSS > Contributions of model... | |||
| Conteúdo da Pasta doc | acessar | |||
| Conteúdo da Pasta source | não têm arquivos | |||
| Conteúdo da Pasta agreement |
| |||
| 4. Condições de acesso e uso | ||||
| Idioma | en | |||
| Grupo de Usuários | administrator marcelo.pazos@inpe.br marciana | |||
| Grupo de Leitores | administrator marcelo.pazos@inpe.br | |||
| Visibilidade | shown | |||
| Política de Arquivamento | denypublisher denyfinaldraft12 | |||
| Permissão de Leitura | deny from all and allow from 150.163 | |||
| Permissão de Atualização | não transferida | |||
| 5. Fontes relacionadas | ||||
| Repositório Espelho | iconet.com.br/banon/2006/11.26.21.31 | |||
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/446B2HE | |||
| Lista de Itens Citando | sid.inpe.br/bibdigital/2021/02.11.21.02 2 sid.inpe.br/mtc-m21/2012/07.13.14.39.50 1 | |||
| Divulgação | WEBSCI; PORTALCAPES; SCOPUS. | |||
| Acervo Hospedeiro | sid.inpe.br/mtc-m19@80/2009/08.21.17.02 | |||
| 6. Notas | ||||
| Campos Vazios | alternatejournal archivist callnumber copyholder copyright creatorhistory descriptionlevel format isbn label lineage mark nextedition notes orcid parameterlist parentrepositories previousedition previouslowerunit progress rightsholder schedulinginformation secondarydate session shorttitle sponsor subject targetfile tertiarymark tertiarytype url | |||
| 7. Controle da descrição | ||||
| e-Mail (login) | marcelo.pazos@inpe.br | |||
| atualizar | ||||